computational logic
Weighted Assumption Based Argumentation to reason about ethical principles and actions
Baldi, Paolo, D'Asaro, Fabio Aurelio, Dyoub, Abeer, Lisi, Francesca Alessandra
We augment Assumption Based Argumentation (ABA for short) with weighted argumentation. In a nutshell, we assign weights to arguments and then derive the weight of attacks between ABA arguments. We illustrate our proposal through running examples in the field of ethical reasoning, and present an implementation based on Answer Set Programming.
Executing Arithmetic: Fine-Tuning Large Language Models as Turing Machines
Lai, Junyu, Xu, Jiahe, Yang, Yao, Huang, Yunpeng, Cao, Chun, Xu, Jingwei
Large Language Models (LLMs) have demonstrated remarkable capabilities across a wide range of natural language processing and reasoning tasks. However, their performance in the foundational domain of arithmetic remains unsatisfactory. When dealing with arithmetic tasks, LLMs often memorize specific examples rather than learning the underlying computational logic, limiting their ability to generalize to new problems. In this paper, we propose a Composable Arithmetic Execution Framework (CAEF) that enables LLMs to learn to execute step-by-step computations by emulating Turing Machines, thereby gaining a genuine understanding of computational logic. Moreover, the proposed framework is highly scalable, allowing composing learned operators to significantly reduce the difficulty of learning complex operators. In our evaluation, CAEF achieves nearly 100% accuracy across seven common mathematical operations on the LLaMA 3.1-8B model, effectively supporting computations involving operands with up to 100 digits, a level where GPT-4o falls short noticeably in some settings.
LLM-FuncMapper: Function Identification for Interpreting Complex Clauses in Building Codes via LLM
Zheng, Zhe, Chen, Ke-Yin, Cao, Xin-Yu, Lu, Xin-Zheng, Lin, Jia-Rui
As a vital stage of automated rule checking (ARC), rule interpretation of regulatory texts requires considerable effort. However, interpreting regulatory clauses with implicit properties or complex computational logic is still challenging due to the lack of domain knowledge and limited expressibility of conventional logic representations. Thus, LLM-FuncMapper, an approach to identifying predefined functions needed to interpret various regulatory clauses based on the large language model (LLM), is proposed. First, by systematically analysis of building codes, a series of atomic functions are defined to capture shared computational logics of implicit properties and complex constraints, creating a database of common blocks for interpreting regulatory clauses. Then, a prompt template with the chain of thought is developed and further enhanced with a classification-based tuning strategy, to enable common LLMs for effective function identification. Finally, the proposed approach is validated with statistical analysis, experiments, and proof of concept. Statistical analysis reveals a long-tail distribution and high expressibility of the developed function database, with which almost 100% of computer-processible clauses can be interpreted and represented as computer-executable codes. Experiments show that LLM-FuncMapper achieve promising results in identifying relevant predefined functions for rule interpretation. Further proof of concept in automated rule interpretation also demonstrates the possibility of LLM-FuncMapper in interpreting complex regulatory clauses. To the best of our knowledge, this study is the first attempt to introduce LLM for understanding and interpreting complex regulatory clauses, which may shed light on further adoption of LLM in the construction domain.
Stress Propagation in Human-Robot Teams Based on Computational Logic Model
Shmerko, Peter, Iwashita, Yumi, Stoica, Adrian, Yanushkevich, Svetlana
Mission teams are exposed to the emotional toll of life and death decisions. These are small groups of specially trained people supported by intelligent machines for dealing with stressful environments and scenarios. We developed a composite model for stress monitoring in such teams of human and autonomous machines. This modelling aims to identify the conditions that may contribute to mission failure. The proposed model is composed of three parts: 1) a computational logic part that statically describes the stress states of teammates; 2) a decision part that manifests the mission status at any time; 3) a stress propagation part based on standard Susceptible-Infected-Susceptible (SIS) paradigm. In contrast to the approaches such as agent-based, random-walk and game models, the proposed model combines various mechanisms to satisfy the conditions of stress propagation in small groups. Our core approach involves data structures such as decision tables and decision diagrams. These tools are adaptable to human-machine teaming as well.
Beginners Learning Path for Machine Learning
Made your mind towards machine learning but are confused so much that where to get started. I faced the same confusion that what should be a good start? Should I learn Python, or go for R? Mathematics was always a scary part for me and I was always worried that from where should I learn math? I was also worried that how should I get a strong basis for Machine Learning. Anyways you should be congratulated that at least you have made your mind.
Logical Judges Challenge Human Judges on the Strange Case of B.C.-Valjean
Mascardi, Viviana, Pellegrini, Domenico
The connections between logic programming and law have been studied for a long time. In 1975, Meldman discussed his PhD Thesis entitled "A preliminary study in computer-aided legal analysis" [12] where he modelled legal facts in a Lisp-like language and used instantiation (recalling unification) and syllogism (recalling resolution) to perform a simple kind of legal analysis inspired by Prosser's Law of Torts [13]. At that time Prolog was just born, but its applications to legal reasoning were not long in coming. One of the first attempts was made by Hustler [9] who implemented a prototype of a legal consultant in Prolog, again inspired by Prosser's work. A few years later, Kowalski, Sergot et al. succeeded in running a significant portion of the 1981 British Nationality Act, implemented in Prolog on a small micro computer [15]. In the same years, Prolog became very popular for implementing expert systems for the legal domain [3, 19]. From those early attempts, much progress has been made: research on deontic and defeasible reasoning [1, 5], ontological reasoning [7], and argumentation [8, 18] is extremely lively and helps disclosing the many connections between logic programming (and, more in general, computational logic and automated reasoning) and legal reasoning. The application of automated reasoning to digital forensics is another promising research direction [6] whose potential is witnessed by the ongoing "Digital Forensics: Evidence Analysis via Intelligent Systems and Practices" (DigForASP) COST Action
Bernard Meltzer, Obituary
Born in South Africa, he was educated at the South African College High School, took a first degree at the University of Cape Town in 1934 and a doctorate in Mathematical Physics at the University of London in 1953. After a spell as demonstrator in physics at Cape Town, he emigrated to Britain. Prior to the outbreak of the Second World War, he undertook ionospheric research in Marconi's Wireless Telegraph Company, transferring to the Government's Telecommunications Research Establishment after the outbreak of hostilities to carry out research on radar. In 1941, he enlisted in the Royal Air Force Volunteer Reserve, leaving in 1943 to go to Aberdeen University to run a special degree course for radio officers under the wartime Hankey Scheme. After the war was over, he returned to industrial research, first until 1949 in Mullard's Radio Valve Company on microwave electronics and then on television and photo-electric tubes at EMI's Research Laboratories.
Description Logics Courses and Tutorials
Enrico Franconi's Course on Description Logics The material includes slides for 6 modules ( 320 slides): A review of Computational Logics, Structural Description Logics, Propositional Description Logics, Description Logics and Knowledge Bases, Description Logics and Logics, Description Logics and Databases. A web pointer to an online modified version of CRACK, allowing for tracing satisfiability proofs with tableaux, is provided. Pointers to relevant online literature are provided, too. Enrico Franconi's Course on Description Logics The material includes slides for 6 modules ( 320 slides): A review of Computational Logics, Structural Description Logics, Propositional Description Logics, Description Logics and Knowledge Bases, Description Logics and Logics, Description Logics and Databases. A web pointer to an online modified version of CRACK, allowing for tracing satisfiability proofs with tableaux, is provided.
4 Building-in Equational Theories G. D. Plotkin
INTRODUCTION If let loose, resolution theorem-provers can waste time in many ways. They can continually rearrange the multiplication brackets of an associative multiplication operation or replace terms t by ones like f(f(f(t, e), e), e) where f is a multiplication function and e is its identity. Generally they continually discover and misapply trivial lemmas. Global heuristics using term complexity do not help much and ad hoc devices seem suspicious. On the other hand, one would like to evaluate terms when possible, for example we would want to replace 5 4 by 9. More generally one would like to have liberty to simplify, to factorise and to rearrange terms. The obvious way to deal with an associative multiplication would be to imitate people, and just drop the multiplication brackets. However used or abused the basic facts involved in such manipulations form an equational theory, T, that is, a theory all of whose sentences are universal closures of equations. Under certain conditions, we will be able to build the equational theory into the rules of inference. The resulting method will be resolution-like, the difference being that concepts are defined using provable equality between terms rather than literal identity. Therefore the set of clauses expressing the theory will not be among the input clauses, so no time will be wasted in the misapplication of trivial lemmas, since the rules will not waste time in this way.